\begin{tabbing}
$\forall$${\it es}$:ES, $e$:E, $l$:IdLnk, ${\it tg}$:Id, $T$:Type, $v$:$T$.
\\[0ex](\{$m$\=:Msg$\mid$ source(mlnk($m$)) = source($l$) $\in$ Id\} \+
\\[0ex]$\subseteq$r Msg($\lambda$${\it l'}$,${\it tg'}$. if ${\it l'}$ = $l$ $\wedge_{b}$ ${\it tg'}$ = ${\it tg}$ then $T$ else Top fi ))
\-\\[0ex]$\Rightarrow$ (\=sends($l$;$e$)\+
\\[0ex]=
\\[0ex][msg($l$;${\it tg}$;$v$)]
\\[0ex]$\in$ (Msg($\lambda$${\it l'}$,${\it tg'}$. if ${\it l'}$ = $l$ $\wedge_{b}$ ${\it tg'}$ = ${\it tg}$ then $T$ else Top fi ) List))
\-\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:E\+
\\[0ex](((kind(${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd) c$\wedge$ (val(${\it e'}$) = $v$ \& sender(${\it e'}$) = $e$))
\\[0ex]\& ($\forall$${\it e''}$:E. (kind(${\it e''}$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (sender(${\it e''}$) = $e$) $\Rightarrow$ (${\it e''}$ = ${\it e'}$))))
\-
\end{tabbing}